Im Bereich der Termersetzungssysteme wird der hierarchisch parallele Hochleistungsbeweiser Teamwork-PaReDuX entwickelt. Teamwork-PaReDuX vereinigt den parallelen Beweiser PaReDuX mit dem verteilten Beweiser Discount, der die Teamwork Methode implementiert. Hierdurch entsteht ein hierarchisch paralleles System, das Netzwerke von modernen parallelen Arbeitsplatzrechnern effizient nutzen und somit signifikante Leistungssteigerungen erzielen kann. Erste Ergebnisse mit dem System auf zwei SPARCstations mit je 4 Prozessoren zeigen z.T. starke superlineare Beschleunigungen. Gleichzeitig wird eine Programmierumgebung geschaffen, die paralleles und verteiltes symbolisches Rechnen allgemein unterstützt.
Teamwork-PaReDuX ist ein Gemeinschaftsprojekt mit der Arbeitsgruppe von Prof. J. Avenhaus von der Fakultät für Informatik der Universität Kaiserslautern. Das Projekt wird seit Ende 1996 durch die DFG im Schwerpunktprogramm ,,Deduktion`` gefördert.
Dr. Beatrice Amrhein